%\documentclass[runningheads]{llncs}
\documentclass[final]{ieee}

\usepackage{microtype} %This gives MUCH better PDF results!
%\usepackage[active]{srcltx} %DVI search
\usepackage[cmex10]{amsmath}
\usepackage{amssymb}
\usepackage{fnbreak} %warn for split footnotes
\usepackage{url}
%\usepackage{qtree} %for drawing trees
%\usepackage{fancybox} % if we need rounded corners
%\usepackage{pict2e} % large circles can be drawn
%\usepackage{courier} %for using courier in texttt{}
%\usepackage{nth} %allows to \nth{4} to make 1st 2nd, etc.
%\usepackage{subfigure} %allows to have side-by-side figures
%\usepackage{booktabs} %nice tables
%\usepackage{multirow} %allow multiple cells with rows in tabular
\usepackage[utf8]{inputenc} % allows to write Faugere correctly
\usepackage[bookmarks=true, citecolor=black, linkcolor=black, colorlinks=true]{hyperref}
\hypersetup{
pdfauthor = {Mate Soos, Bart Selman, Henry Kautz},
pdftitle = {CryptoMiniSat v5.6 + walksat},
pdfsubject = {SAT Competition 2020},
pdfkeywords = {SAT Solver, DPLL, SLS},
pdfcreator = {PdfLaTeX with hyperref package},
pdfproducer = {PdfLaTex}}
%\usepackage{butterma}

%\usepackage{pstricks}
\usepackage{graphicx,epsfig,xcolor}

\begin{document}
\title{CryptoMiniSat with WalkSAT at the SAT Competition 2020}
\author{Mate Soos (National University of Singapore)\\
Bart Selman (Cornell University), Henry Kautz (University of Rochester)\\
Jo Devriendt, Stephan Gocht (Lund University \& University of Copenhagen)}

\maketitle
\thispagestyle{empty}
\pagestyle{empty}

\section{Introduction}
This paper presents the conflict-driven clause-learning (CLDL) SAT solver CryptoMiniSat (\emph{CMS}) augmented with the Stochastic Local Search (SLS)~\cite{Selman95localsearch} solver WalkSAT v56 as submitted to SAT Competition 2020.

CryptoMiniSat aims to be a modern, open source SAT solver using inprocessing techniques, optimized data structures and finely-tuned timeouts to have good control over both memory and time usage of inprocessing steps. CryptoMiniSat is authored by Mate Soos.

WalkSAT~\cite{DBLP:conf/aaai/KautzS96} is a standard system to solve satisfiability problems using Stochastic Local Search. The version inside CryptoMiniSat is functionally equivalent to the ``rnovelity'' heuristic of WalkSAT v56 using an adaptive noise heuristic~\cite{DBLP:conf/aaai/Hoos02}. It behaves exactly as WalkSAT with the minor modification of performing early-abort in case the ``lowbad'' statistic (i.e. the quality indicator of the current best solution) indicates the solution is far. In these cases, we early abort, let the CDCL solver work longer to simplify the problem, and come back to WalkSAT later. The only major modification to WalkSAT has been to allow it to import variables and clauses directly from the main solver taking into account assumptions given by the user.

\section{Composing the Two Solvers}
The two solvers are composed together in a way that does \emph{not} resemble portfolio solvers. The system runs the CDCL solver CryptoMiniSat, along with its periodic inprocessing, by default. However, at every 2nd inprocessing step, CryptoMiniSat's irredundant clauses are pushed into the SLS solver (in case the predicted memory use is not too high). The SLS solver is then allowed to run for a predefined number of steps. In case the SLS solver finds a solution, this is given back to the CDCL solver, which then performs all the necessary extension to the solution (e.g. for Bounded Variable Elimination, BVE~\cite{BVE}) and then outputs the solution.

Note that the inclusion of the SLS solver is full in the sense that assumptions-based solving, library-based solver use, and all other uses of the SAT solver is fully supported with SLS solving enabled. Hence, this is not some form of portfolio where a simple shell script determines which solver to run and then runs that solver. Instead, the SLS solver is a full member of the CDCL solver, much like any other inprocessing system, and works in tandem with it. For example, in case an inprocessing step has reduced the number of variables through BVE or increased it through BVA~\cite{BVA}, the SLS solver will then try to solve the problem thus modified. In case the SLS solver finds a solution, the main solver will then correctly manipulate it to fit the needs of the ``outside world'', i.e. the caller.

As the two solvers are well-coupled, the combination of the two solvers can solve problems that neither system can solve on its own. Hence, \emph{the system is more than just a union of its parts} which is not the case for traditional portfolio solvers.

\section{Gauss-Jordan Elimination}
As per the upcoming paper~\cite{birdtwo}, the Gauss-Jordan elimination of CryptoMiniSat has been significantly improved. The average speed increase for moderately sized matrices is approx 3-6x, allowing the system to be ran at all times even when the matrix is not contributing as much to the overall solving. Hence, for the first time in CryptoMiniSat's 10 year history, Gauss-Jordan elimination is turned on by default for the NoLimits track.


\section{Symmetry Breaking using BreakID and Bliss}
The BreakID~\cite{breakid2016} system is a cost-effective symmetry breaking preprocessor for SAT.
Classic SAT symmetry preprocessing~\cite{shatter2006} detects symmetry by converting the input formula to a graph and computing generators for this graph's automorphism group, and adds symmetry breaking clauses on a generator-by-generator basis.
On top of this, BreakID heuristically searches for structure in the automorphism group, detecting \emph{row interchangeability symmetry} (such as in the pigeonhole problem) and computing binary symmetry breaking clauses from orbits arising from the symmetry group.
The resulting symmetry breaking clauses are more effective at reducing symmetrical assignments from the search space, both from a theory point of view as well as in practical experiments.

BreakID has been modified to work as a library. It can receive the clauses on-the-fly from the SAT solver, and produce the breaking clauses as a function return value. Various small bugs have also be fixed, such as memory leaks, which were not an issue when ran as a single executable, but created isses when ran as a library. Furthermore, the underlying highly sophisticated graph automorphism detection system, Bliss~\cite{DBLP:conf/alenex/JunttilaK07}, has been slightly improved to allow for time-outs and it, too, has been fixed not to leak memory. BreakID is fully integrated into CryptoMiniSat by calling it on every 5th inprocessing iteration, and asked to contribute breaking clauses. These are always added with an assumption literal, so they can be removed when the solving finishes. Hence, symmetry breaking also works when CryptoMiniSat is used as a library.


\section{Further Improvements Relative to SAT Race 2019}
Many of the inprocessing parameters have been tuned. A few bugs related to clause activities have been fixed. Clause distillation (or clause vivification)~\cite{DBLP:journals/ai/LiXLMLL20} is now used a lot more, similarly to the previous years' winning solvers. The VSIDS and Maple decay factors are now iteratively changed between 0.70 and 0.90 for Maple and 0.92 and 0.99 for VSIDS. Between each iteration there is an inprocessing step, as before. This seems to add heterogeneity and avoids having to tune these parameters to a ``single best'' value. Polarity caching is still used, but once in a while, so-called ``stable'' polarities are used, as per CaDiCaL~\cite{cadical} in the SAT Race of 2019. Ternary resolution is also used at every inprocessing step, thanks to the suggestion by Armin Biere.


\section{Thanks}
Mate Soos was supported in part by the National Research Foundation Singapore under its NRF Fellowship Programme[NRF-NRFFAI1-2019-0004 ] and AI Singapore Programme [AISG-RP-2018-005],  and NUS ODPRT Grant [R-252-000-685-13].

Stephan Gocht was funded by the Swedish Research Council (VR) grant \mbox{2016-00782}.

The computational work for this article was performed on resources of the National Supercomputing Center, Singapore\cite{nscc}. Mate Soos would also like to thank all the users of CryptoMiniSat who have submitted over 600 issues and pull requests to the GitHub CMS repository\cite{CMS}.

\bibliographystyle{splncs03}
\bibliography{sigproc}

\vfill
\pagebreak

\end{document}

